effect{-}type(${\it ds}$;${\it ds'}$;${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$${\it kx}$:Knd$\times$Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;1of(${\it kx}$))$\rightarrow$fpf{-}cap(${\it ds'}$;IdDeq;2of(${\it kx}$);Top)